Lambda the Ultimate

Hi there,

Sorry to pester y'all, but I was hoping I might get some citation-type help. I realized for my little pet language that I'm working on that need to do some homework on conjunction types, but I can't find any publicly-available articles on the topic. Does anyone know off of the top of their heads any friendly introductions to these types that doesn't require IEEE or ACM membership to read?

Thanks in advance,

JimDesu

I've been reading a lot about various new languages like Ruby, Haskell, Python, etc. But none of them seem suitable for programming say, an Operating System, or performing really low level work on an embedded device. First, these languages (understandably) sacrifice efficiency for ease of use (but I don't think these are always mutually exclusive). Second, a lot of times these languages simply don't provide any mechanism for getting at the hardware.

Has there been any research into new languages that would be as suitable for an OS as C?

I am pondering over some non-serious application of Curry-Howard isomorphism (CHI). Let's take any typical text in a natural language. What is its contents? Propositions or proofs? My judgement is that (almost?) exclusively propositions. Applying CHI, we can see that humans write mostly types. Already sounds strange.

Now, instead of a static text, let's analyze an interaction in a natural language (e.g., a conversation over a phone). People are still exchanging propositions, i.e., types. From this point I am trying to get back to computer science. Why isn't it so common that programs exchange types over the wire? Or rather, why cant we naturally see any programmatic interaction as an exchange of (exclusively) types? I suspect we can argue that transmitted values are just witnesses of the corresponding types, but still it is not natural, or at least traditional way to look at the issue. Why? Or did I make some mistake during my analysis of natural language part of the problem?

I know that "programmatic interaction" can be seen as a proof-reduction, but I am currently wearing more message-oriented hat.

A few years back (back around the year 86 or 87 to those who really care) when I worked at Digital Equipment Corporation, I caused a bit of a stir by entering a new "Note" in the Languages notesfile (which was one of many VAXNotes notesfiles paving the corporate intranet of DEC back in the days before the internet really existed to any meaningful extent).

The note was entitled "Battle of the Languages" and the idea was that people would have the opportunity to prove the superiority of their particular favorite language by posting the source code for the now somewhat famous computer simulation called "Life" which was invented by the Cambridge mathematician John Conway, and which consisted of the following rules:

For a space that is 'populated':
Each cell with one or no neighbors dies, as if by loneliness.
Each cell with four or more neighbors dies, as if by overpopulation.
Each cell with two or three neighbors survives.
For a space that is 'empty' or 'unpopulated'
Each cell with three neighbors becomes populated.

In an matter of days, there were upwards of twenty different languages represented as replies to the intitial posting (note). I think the language "C" was the first to post a solution followed by Pascal (my current language of choice), as well as many others (sans Java and a few other more recent languages for obvious reasons).

I think I may still even have a backup tape of this and other notesfiles which was made on a VAXstation 2000 back around 1990 or so if anyone is interested, but I digress...

My main point in posting this is to state that I always enjoyed conducting that little experiment and I am not real sure what was really proven (other than the fact that people can certainly be passionate about their favorite computer programming languages).

I am half tempted to conduct the same experiment today, although I imagine that, due to the wonders of Google and other search engines, that the source code listings of some of the more popular languages would appear within minutes rather than hours or days. This would especially be true for a common mathematical simulation like Life, which has already been posted to death many times over.

It might be interesting to see what were to happen if the same contest were conducted using a different simulation candidate however... any takers on what to use for such an experiment and what parameters to set as rules (graphics or text output only, etc.)?

Thanks

-dav0 (aka David McLure - DEC employee from 1984 to 1992)

Recently I noticed several threads bumping up to the top of the tracker without any new posts in them (e.g., this or this). Upon closer examination, it looks they have a quite recent "last post" timestamp, very different from timestamps of contained posts. Is it a bug, or just a consequence of some administrative behavior (e.g., deleting inappropriate posts)?

If the latter, it's an interesting example of a business rule enforced only in one direction - upon creation of a post its timestamp is propagated to the thread, while upon deletion the effect is not undone. Where is a referential transparency?? :-)

I just had an interesting phone conversation with a friend of mine concerning the building of robost software (architectures, applications) and how the process could relate to language design.

We started listing a checklist of criteria (whether required or merely wanted) and we came up with a few items. We had a simple criteria of program correctness, program maintainence (comprehension), and modularity.

For program comprehension/correctness:
Strong typing
Purely functional
Strict evaluation
Design by Contract came up as a possibility
Verbose error messages

For modularity:
Objects were a thought, but it was felt the same architectures could be achieved with types, functions, and modules

These were just a few of the things that we thought could help in building large scale applications and frameworks, but both my friend and I lack the desired amount of experience to develop a stricter and more verbose criteria.

I was wondering what everyone's elses opionion would be concerning this topic.

If you had to build a large software architecture/application what kind of 'features' would you look for in a language?

Best regards,

MJ Stahl

It's been a long while since I've looked at Logo. Somehow I ended up here. Logo is often considered only a toy language. But, while it doesn't have the expressiveness of it's closest cousins Scheme and Lisp, simplicity has it's place.

In primary/secondary education, Squeak Smalltalk seems to be taking away the Logo mindshare (at least it seems this way). Is this true?

Are there any network transparent languages apart from Mozart(Oz) and Google's Sawzall(to some extent).I have tried searching on this subject, but nothing significant turned up.I have not even found any references to such languages in any of the programming language (text) books.

I would be glad if anyone can answer the following questions:
- Are they different from languages which support distributed programming?
- Why are they not popular, i feel that such a language has very interesting and practical applications.( like run-time load balancing of applications etc..)
- Are there any theoritical/practical reasons why they will not be useful, even if one exists?

Any other pointers will also be helpful.

I have a bunch of ideas for my own programming language (like every other CS undergraduate with an appropriate degree of hubris) and I'm starting to fiddle with writing my own compiler for it, but I'm having trouble understanding a lot of technical material out there. Most of the programming language papers and tutorials I'm finding on the net assume that I already know lambda calculus and other advanced mathematics.

What's some good easy to understand stuff I can read to get the mathematical basis I need to understand all the jargon, or understand some if it without the math? (i.e. I'd like to understand dependent typing, but the papers I've found turn my brain into knots)

Functional Pearl: Applicative programming with effects, Conor McBride and Ross Patterson

In this paper, we introduce Applicative functors—an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the ubiquity of this programming pattern that drew us to the abstraction. We retrace our steps in this paper, introducing the applicative pattern by diverse examples, then abstracting it to define the Applicative type class and introducing a bracket notation which interprets the normal application syntax in the idiom of an Applicative functor. Further, we develop the properties of applicative functors and the generic operations they support. We close by identifying the categorical structure of applicative functors and examining their relationship both with Monads and with Arrows.

A well written introduciton to a monad cousin, with a tantilizing hint that idioms are easier to introduce into Haskell syntax:

Given Haskell extended with multi-parameter type classes, enthusiasts for overloading may replace [[ and ]] by identifiers iI and Ii with the right behaviour³.

³ Hint: Define an overloaded function applicative u v1 . . . vn Ii = u (*) v1 ... (*) vn